es:ES, e1:E, e2:{e:E| loc(e) = loc(e1)  Id }, p, q, p',
q':({e:E| loc(e) = loc(e1)  Id }{e:E| loc(e) = loc(e1)  Id }Prop).
(a, b:{e:E| loc(e) = loc(e1)  Id }. (a  [e1, e2])  (b  [e1, e2])  (p(a,b)  p'(a,b)))
 (a, b:{e:E| loc(e) = loc(e1)  Id }. (a  [e1, e2])  (b  [e1, e2])  (q(a,b)  q'(a,b)))
 ([e1;e2]~([a,b].p(a,b))*[a,b].q(a,b)  [e1;e2]~([a,b].p'(a,b))*[a,b].q'(a,b)) 

latex

Definitions	t  T, x:A. B(x), P  Q, P  Q, P & Q, P  Q, ES, E, loc(e), Id, Prop, x(s1,s2), [e, e'], (x  l), {T}, x,y. t(x;y)
Lemmas	es-pstar-q functionality wrt rev implies, l member wf, es-interval wf, iff wf, Id wf, es-loc wf, es-E wf, event system wf, es-pstar-q wf